This is on top of #2017 based on #2017 (comment).

Changes:

• Adds the regression from Fix memOutOfBounds handling of negative pointer offsets #2017 (comment) that exposed the unsoundness
• Fixes dereference bound checks to include offsets already encoded in the pointer's points-to address, instead of only looking at the offset introduced by the current dereference expression
• Refactors the new offset-handling logic into helper functions for readability
• Simplifies BinOp handling by passing the original expression through the checks instead of destructuring and reconstructing it
  • I initially removed the match on BinOp from check_binop_exp altogether because the only place where it is called from is within a match case on BinOp ((PlusPI | MinusPI | IndexPI), ...), but decided to keep it just in case for future, so that it is not called from a wrong place and if it is, would notify with an error message.

This is still not an ideal code structure, as evidenced by the need for comments like:

(* Explicit pointer arithmetic is checked separately by check_binop_exp; do not add it here again. *)

Obviously the overall analysis workflow is a bit non-straightforward if we have to leave comments like this. But that is an issue for another cleanup PR, at least this should fix the unsoundness itself.